Termination of the following Term Rewriting System could be proven:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

from(X) → cons(X, from(s(X)))
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
sel(0, cons(X, Z)) → X
sel(s(X), cons(Y, Z)) → sel(X, Z)

The replacement map contains the following entries:

from: {1}
cons: {1}
s: {1}
first: {1, 2}
0: empty set
nil: empty set
sel: {1, 2}


CSR
  ↳ CSRInnermostProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

from(X) → cons(X, from(s(X)))
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
sel(0, cons(X, Z)) → X
sel(s(X), cons(Y, Z)) → sel(X, Z)

The replacement map contains the following entries:

from: {1}
cons: {1}
s: {1}
first: {1, 2}
0: empty set
nil: empty set
sel: {1, 2}

The CSR is orthogonal. By [10] we can switch to innermost.

↳ CSR
  ↳ CSRInnermostProof
CSR
      ↳ CSDependencyPairsProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

from(X) → cons(X, from(s(X)))
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
sel(0, cons(X, Z)) → X
sel(s(X), cons(Y, Z)) → sel(X, Z)

The replacement map contains the following entries:

from: {1}
cons: {1}
s: {1}
first: {1, 2}
0: empty set
nil: empty set
sel: {1, 2}

Innermost Strategy.

Using Improved CS-DPs we result in the following initial Q-CSDP problem.

↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
QCSDP
          ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {from, s, first, sel, SEL, FROM, FIRST} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DPo are:

SEL(s(X), cons(Y, Z)) → SEL(X, Z)

The collapsing dependency pairs are DPc:

SEL(s(X), cons(Y, Z)) → Z


The hidden terms of R are:

from(s(X))
first(X, Z)

Every hiding context is built from:

s on positions {1}
from on positions {1}
first on positions {1, 2}

Hence, the new unhiding pairs DPu are :

SEL(s(X), cons(Y, Z)) → U(Z)
U(s(x_0)) → U(x_0)
U(from(x_0)) → U(x_0)
U(first(x_0, x_1)) → U(x_0)
U(first(x_0, x_1)) → U(x_1)
U(from(s(X))) → FROM(s(X))
U(first(X, Z)) → FIRST(X, Z)

The TRS R consists of the following rules:

from(X) → cons(X, from(s(X)))
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
sel(0, cons(X, Z)) → X
sel(s(X), cons(Y, Z)) → sel(X, Z)

The set Q consists of the following terms:

from(x0)
first(0, x0)
first(s(x0), cons(x1, x2))
sel(0, cons(x0, x1))
sel(s(x0), cons(x1, x2))


The approximation of the Context-Sensitive Dependency Graph contains 2 SCCs with 3 less nodes.


↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSDependencyGraphProof
            ↳ AND
QCSDP
                ↳ QCSDPSubtermProof
              ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {from, s, first, sel} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {U} are not replacing on any position.

The TRS P consists of the following rules:

U(s(x_0)) → U(x_0)
U(from(x_0)) → U(x_0)
U(first(x_0, x_1)) → U(x_0)
U(first(x_0, x_1)) → U(x_1)

The TRS R consists of the following rules:

from(X) → cons(X, from(s(X)))
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
sel(0, cons(X, Z)) → X
sel(s(X), cons(Y, Z)) → sel(X, Z)

The set Q consists of the following terms:

from(x0)
first(0, x0)
first(s(x0), cons(x1, x2))
sel(0, cons(x0, x1))
sel(s(x0), cons(x1, x2))


We use the subterm processor [20].


The following pairs can be oriented strictly and are deleted.


U(s(x_0)) → U(x_0)
U(from(x_0)) → U(x_0)
U(first(x_0, x_1)) → U(x_0)
U(first(x_0, x_1)) → U(x_1)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
U(x1)  =  x1

Subterm Order


↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSDependencyGraphProof
            ↳ AND
              ↳ QCSDP
                ↳ QCSDPSubtermProof
QCSDP
                    ↳ PIsEmptyProof
              ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {from, s, first, sel} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

from(X) → cons(X, from(s(X)))
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
sel(0, cons(X, Z)) → X
sel(s(X), cons(Y, Z)) → sel(X, Z)

The set Q consists of the following terms:

from(x0)
first(0, x0)
first(s(x0), cons(x1, x2))
sel(0, cons(x0, x1))
sel(s(x0), cons(x1, x2))


The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.

↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSDependencyGraphProof
            ↳ AND
              ↳ QCSDP
QCSDP
                ↳ QCSDPSubtermProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {from, s, first, sel, SEL} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.

The TRS P consists of the following rules:

SEL(s(X), cons(Y, Z)) → SEL(X, Z)

The TRS R consists of the following rules:

from(X) → cons(X, from(s(X)))
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
sel(0, cons(X, Z)) → X
sel(s(X), cons(Y, Z)) → sel(X, Z)

The set Q consists of the following terms:

from(x0)
first(0, x0)
first(s(x0), cons(x1, x2))
sel(0, cons(x0, x1))
sel(s(x0), cons(x1, x2))


We use the subterm processor [20].


The following pairs can be oriented strictly and are deleted.


SEL(s(X), cons(Y, Z)) → SEL(X, Z)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
SEL(x1, x2)  =  x1

Subterm Order


↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSDependencyGraphProof
            ↳ AND
              ↳ QCSDP
              ↳ QCSDP
                ↳ QCSDPSubtermProof
QCSDP
                    ↳ PIsEmptyProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {from, s, first, sel} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

from(X) → cons(X, from(s(X)))
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
sel(0, cons(X, Z)) → X
sel(s(X), cons(Y, Z)) → sel(X, Z)

The set Q consists of the following terms:

from(x0)
first(0, x0)
first(s(x0), cons(x1, x2))
sel(0, cons(x0, x1))
sel(s(x0), cons(x1, x2))


The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.